Modern integrated circuits (ICs) are often very large and complex, and may be built from tens or even hundreds of millions of transistors, making these systems difficult and expensive to design and validate. Market demands may require ICs to possess ever-increasing performance, advanced feature sets, system versatility, and a variety of other rapidly changing system specifications. These demands often introduce contradictory design requirements into the design process. Circuit designers are required to make significant tradeoffs in performance, physical size, architectural complexity, power consumption, heat dissipation, fabrication complexity, and cost, among others, to try to meet design requirements best. Each design decision exercises a profound influence on the resulting IC. To handle such IC complexity, designers create specifications and design ICs around the specifications. The specifications attempt to balance the many disparate demands being made of the ICs and contain the ever-increasing design complexity.
The process of comparing proposed designs to the specifications around which they were constructed helps ensure that the designs meet critical IC objectives. The process of comparing two or more designs is called verification. Logic systems may be described at a variety of levels of abstraction, from low-level transistor layouts to high-level description languages. Circuit designers can describe and design their ICs at a high-level of abstraction using an IEEE Standard hardware description language (HDL) such as Verilog™, SystemVerilog™, or VHDL™ Often, a high-level HDL is easier for designers to understand, especially for a vast system, as the high-level HDL may describe highly complex concepts that are difficult to grasp using a lower level of abstraction. An HDL description may be converted into another, lower level of abstraction if helpful to the circuit designers. For example, a high-level description may be converted to a logic-level description such as a register-transfer level (RTL), a gate-level (GL) description, a layout-level description, or a mask-level description. Each lower level of abstraction introduces more detail into the design description.
Circuit designs of ICs can be optimized at a lower level of abstraction than high-level HDL, such as RTL, in order to reduce the time-to-market of ICs. During optimizations at RTL, two or more circuit designs can be compared to verify that the designs exhibit identical functional behavior. Sequential Equivalence Checking (SEC) is a technique designed to compare two circuit designs and verify that they are equivalent on a cycle-by-cycle basis. A variety of advanced techniques, such as black-boxing and abstract logic models, can be deployed to overcome the resource constraints and the fundamental limitation of formal algorithms, and simplify the SEC. For a given SEC setup, there are three possible outcomes: (i) the designs are verified to be equivalent based on the given setup, (ii) the designs were not equivalent, and (iii) the verification was inconclusive. When the designs are not equivalent, the circuit designer may try to debug a counter-example generated by the SEC setup and identify the possible cause of the differences in the designs. If verification of the designs were inconclusive, the user might be required to identify the potential regions in the circuit designs that may be causing the differences.
An SEC setup of a first circuit design and a second circuit design can be broken into multiple potential equivalent sub-circuit pairs at a register transfer level where each pair identifies with a sub-circuit of the first design and a sub-circuit of the second design. The sub-circuits of the first and second designs have similar functionality and variables of interest (observables such as inputs and outputs) at RTL. The potential equivalent sub-circuit pairs can be identified by their relative position with respect to the time domain (clock cycles), or their position in the space domain of the two circuit designs. The multiple potential equivalent sub-circuit pairs can be sequentially compared, making the SEC process a time-consuming and complex project.
It is therefore desirable to provide SEC system that verifies the two circuit designs in a methodical and time-efficient way, thereby, improving the quality of debugging and ability to pinpoint the exact locations of the design differences. It is also desirable to provide the circuit designers with an activity viewer that dynamically tracks the SEC process.